/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.bool;

import alloy.util.Dbg;

/**
 * Computes a simplification of the given {@link BooleanFormula} with the given
 * {@link PartialAssignment}.  The simplified formula does not reference any
 * variables assigned by the partial assignment, or any constants (unless
 * the entire formula simplifies to a constant).  Sharing of nodes in the
 * visited Boolean DAG is preserved; but, of course, if you had external pointers
 * into the DAG, they will not be changed to point to simplified nodes.
 * <p>
 * The forXXXX methods return the simplified version of the boolean formula.
 * No Boolean nodes are mutated; the simplified version may shared subtrees
 * with the original Boolean DAG, but when modifications are needed, new
 * Boolean nodes are created to represent the simplified DAG.
 * <p>
 * The DAG being simplified must consist solely of AND/OR/NOT/Literal/Constant nodes;
 * if any other node types are present, an error will be thrown.
 *
 * @see BooleanFormula#simplify
 * @see Eval_V
 */
class BoolSimplifyVisitor extends GBF_V {
    /**
     * The {@link PartialAssignment} with which we are simplifying the formula.
     * Allows us to treat some {@link GBF_Lit} nodes as {@link GBF_Const}.
     */
    private PartialAssignment _pa;

    /**
     * Scratch area used for constructing child lists for AND/OR nodes.
     * It's a static area so the code is non-reentrant.
     */
    private static BooleanFormula[] _sScratch = new BooleanFormula[1024];

    public static void initSingleton() {
    	_sScratch = null;
    	_sScratch = new BooleanFormula[1024];
    }
    
    //////////////
    // Methods //
    ////////////

    BoolSimplifyVisitor(PartialAssignment pa_) { _pa = pa_; }

    /**
     * Ensure that the array {@link #_sScratch} has at least the given size.
     * Any current data in the array is preserved.
     */
    private static void _ensureScratchSize(int minSize_) {
	int newSize = _sScratch.length;
	while (newSize < minSize_)
	    newSize *= 2;
	Dbg.chk(newSize>0);
	if (newSize > _sScratch.length) {
	    BooleanFormula[] newScratch = new BooleanFormula[newSize];
	    System.arraycopy(_sScratch, 0, newScratch, 0, _sScratch.length);
	    _sScratch = newScratch;
	}
    }  // _ensureScratchSize()

    Object forConst(GBF_Const g_const) { return g_const; }
    Object forLit(GBF_Lit g_lit) {
	int lit = g_lit.getLit();
	int var = lit>0 ? lit : -lit;
	return _pa.isAssigned(var) ?
	    BooleanFormula.makeConst(_pa.getLitValue(lit)) : g_lit;
    }

    Object forNot(GBF_Not g_not) {
	if (alreadyVisited(g_not))
	    return g_not.lastVisitorResult;
	BooleanFormula simplifiedChild = (BooleanFormula)g_not.expr.acceptVisitor(this);
	if (simplifiedChild == g_not.expr)
	    return g_not;
	return simplifiedChild.not();
    }

    private Object _forAndOr(GBF_AndOrBase andor_, boolean isAnd_) {
	if (alreadyVisited(andor_))
	    return andor_.lastVisitorResult;
	int newChildCount = 0;
	BooleanFormula[] subexprs = andor_.subexprs;
	_ensureScratchSize(subexprs.length);
	boolean someChildChanged = false;
	for (int i=0; i<subexprs.length; i++) {
	    BooleanFormula simpl = (BooleanFormula)subexprs[i].acceptVisitor(this);
	    someChildChanged |= (simpl != subexprs[i]);
	    if ((isAnd_ && simpl == BooleanFormula.FALSE()) ||
		(!isAnd_ && simpl == BooleanFormula.TRUE()))
		return simpl;
	    if ((isAnd_ && simpl == BooleanFormula.TRUE()) ||
		(!isAnd_ && simpl == BooleanFormula.FALSE()))
		continue;

	    _sScratch[newChildCount++] = simpl;
	}
	if (newChildCount == 0) return isAnd_ ? BooleanFormula.TRUE() : BooleanFormula.FALSE();
	if (newChildCount == 1) return _sScratch[0];
	if (!someChildChanged) return andor_;
	BooleanFormula[] newChildList = new BooleanFormula[newChildCount];
	System.arraycopy(_sScratch, 0, newChildList, 0, newChildCount);
	return isAnd_ ? (BooleanFormula)new GBF_And(newChildList) : (BooleanFormula)new GBF_Or(newChildList);
    }

    public Object forAnd(GBF_And and_) { return _forAndOr(and_, true); }
    public Object forOr(GBF_Or or_) { return _forAndOr(or_, false); }

    public Object forCNFFunc(CNFFunc cnfFunc_) { throw new Error("should not happen"); }
    
    public Object forSetVarExpr(SetVarExpr setVarExpr_) {
	throw new Error("should not happen");
    }

    public Object forVarConst(VarConst varConst_) {
	throw new Error("should not happen");
    }
}
